YES 1.5070000000000001 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  (((/=) :: Eq a => Maybe a  ->  Maybe a  ->  Bool) :: Eq a => Maybe a  ->  Maybe a  ->  Bool)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  (((/=) :: Eq a => Maybe a  ->  Maybe a  ->  Bool) :: Eq a => Maybe a  ->  Maybe a  ->  Bool)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  ((/=) :: Eq a => Maybe a  ->  Maybe a  ->  Bool)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xv2100), Succ(xv401000)) → new_primPlusNat(xv2100, xv401000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xv30100), Succ(xv40100)) → new_primMulNat(xv30100, Succ(xv40100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xv3000), Succ(xv4000)) → new_primEqNat(xv3000, xv4000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_esEs(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_@2, cc), cd), ce) → new_esEs(xv300, xv400, cc, cd)
new_esEs(@2(xv300, xv301), @2(xv400, xv401), app(ty_[], cf), ce) → new_esEs0(xv300, xv400, cf)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, ba), app(app(ty_Either, be), bf))) → new_esEs1(xv301, xv401, be, bf)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(app(ty_@3, bcg), bch), bda)), hf), bbb)) → new_esEs2(xv300, xv400, bcg, bch, bda)
new_esEs1(Right(xv300), Right(xv400), gc, app(ty_Maybe, hd)) → new_esEs3(xv300, xv400, hd)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, hf, app(ty_[], baa)) → new_esEs0(xv302, xv402, baa)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, he), hf), app(app(ty_Either, bab), bac))) → new_esEs1(xv302, xv402, bab, bac)
new_esEs1(Left(xv300), Left(xv400), app(ty_[], fc), fb) → new_esEs0(xv300, xv400, fc)
new_esEs(@2(xv300, xv301), @2(xv400, xv401), app(ty_Maybe, de), ce) → new_esEs3(xv300, xv400, de)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, hf, app(ty_Maybe, bag)) → new_esEs3(xv302, xv402, bag)
new_esEs3(Just(Left(xv300)), Just(Left(xv400)), app(app(ty_Either, app(app(ty_Either, fd), ff)), fb)) → new_esEs1(xv300, xv400, fd, ff)
new_esEs1(Left(xv300), Left(xv400), app(app(ty_Either, fd), ff), fb) → new_esEs1(xv300, xv400, fd, ff)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, app(app(app(ty_@3, db), dc), dd)), ce)) → new_esEs2(xv300, xv400, db, dc, dd)
new_esEs3(Just(:(xv300, xv301)), Just(:(xv400, xv401)), app(ty_[], app(ty_[], ea))) → new_esEs0(xv300, xv400, ea)
new_esEs3(Just(Right(xv300)), Just(Right(xv400)), app(app(ty_Either, gc), app(ty_[], gf))) → new_esEs0(xv300, xv400, gf)
new_esEs1(Right(xv300), Right(xv400), gc, app(app(ty_@2, gd), ge)) → new_esEs(xv300, xv400, gd, ge)
new_esEs3(Just(Right(xv300)), Just(Right(xv400)), app(app(ty_Either, gc), app(app(ty_Either, gg), gh))) → new_esEs1(xv300, xv400, gg, gh)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(ty_@2, bcb), bcc)), hf), bbb)) → new_esEs(xv300, xv400, bcb, bcc)
new_esEs3(Just(Left(xv300)), Just(Left(xv400)), app(app(ty_Either, app(app(ty_@2, eh), fa)), fb)) → new_esEs(xv300, xv400, eh, fa)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, app(ty_Maybe, de)), ce)) → new_esEs3(xv300, xv400, de)
new_esEs(@2(xv300, xv301), @2(xv400, xv401), ba, app(app(ty_Either, be), bf)) → new_esEs1(xv301, xv401, be, bf)
new_esEs(@2(xv300, xv301), @2(xv400, xv401), ba, app(ty_[], bd)) → new_esEs0(xv301, xv401, bd)
new_esEs(@2(xv300, xv301), @2(xv400, xv401), ba, app(app(ty_@2, bb), bc)) → new_esEs(xv301, xv401, bb, bc)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, he), hf), app(ty_[], baa))) → new_esEs0(xv302, xv402, baa)
new_esEs(@2(xv300, xv301), @2(xv400, xv401), app(app(app(ty_@3, db), dc), dd), ce) → new_esEs2(xv300, xv400, db, dc, dd)
new_esEs1(Left(xv300), Left(xv400), app(ty_Maybe, gb), fb) → new_esEs3(xv300, xv400, gb)
new_esEs1(Left(xv300), Left(xv400), app(app(ty_@2, eh), fa), fb) → new_esEs(xv300, xv400, eh, fa)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_@2, bcb), bcc), hf, bbb) → new_esEs(xv300, xv400, bcb, bcc)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, app(app(ty_Either, cg), da)), ce)) → new_esEs1(xv300, xv400, cg, da)
new_esEs3(Just(Left(xv300)), Just(Left(xv400)), app(app(ty_Either, app(ty_[], fc)), fb)) → new_esEs0(xv300, xv400, fc)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_[], bcd), hf, bbb) → new_esEs0(xv300, xv400, bcd)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, he), hf), app(app(app(ty_@3, bad), bae), baf))) → new_esEs2(xv302, xv402, bad, bae, baf)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, app(ty_[], bbc), bbb) → new_esEs0(xv301, xv401, bbc)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, he), hf), app(app(ty_@2, hg), hh))) → new_esEs(xv302, xv402, hg, hh)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(ty_[], bcd)), hf), bbb)) → new_esEs0(xv300, xv400, bcd)
new_esEs(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_Either, cg), da), ce) → new_esEs1(xv300, xv400, cg, da)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, he), app(app(ty_Either, bbd), bbe)), bbb)) → new_esEs1(xv301, xv401, bbd, bbe)
new_esEs0(:(xv300, xv301), :(xv400, xv401), df) → new_esEs0(xv301, xv401, df)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, hf, app(app(app(ty_@3, bad), bae), baf)) → new_esEs2(xv302, xv402, bad, bae, baf)
new_esEs3(Just(Left(xv300)), Just(Left(xv400)), app(app(ty_Either, app(app(app(ty_@3, fg), fh), ga)), fb)) → new_esEs2(xv300, xv400, fg, fh, ga)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, hf, app(app(ty_Either, bab), bac)) → new_esEs1(xv302, xv402, bab, bac)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(app(ty_@3, bcg), bch), bda), hf, bbb) → new_esEs2(xv300, xv400, bcg, bch, bda)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, ba), app(app(app(ty_@3, bg), bh), ca))) → new_esEs2(xv301, xv401, bg, bh, ca)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(ty_Maybe, eg)) → new_esEs3(xv300, xv400, eg)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(ty_Maybe, bdb)), hf), bbb)) → new_esEs3(xv300, xv400, bdb)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, app(ty_Maybe, bca), bbb) → new_esEs3(xv301, xv401, bca)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, he), app(app(ty_@2, bah), bba)), bbb)) → new_esEs(xv301, xv401, bah, bba)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, ba), app(ty_Maybe, cb))) → new_esEs3(xv301, xv401, cb)
new_esEs3(Just(:(xv300, xv301)), Just(:(xv400, xv401)), app(ty_[], app(app(ty_@2, dg), dh))) → new_esEs(xv300, xv400, dg, dh)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(app(app(ty_@3, ed), ee), ef)) → new_esEs2(xv300, xv400, ed, ee, ef)
new_esEs1(Right(xv300), Right(xv400), gc, app(ty_[], gf)) → new_esEs0(xv300, xv400, gf)
new_esEs1(Right(xv300), Right(xv400), gc, app(app(ty_Either, gg), gh)) → new_esEs1(xv300, xv400, gg, gh)
new_esEs3(Just(:(xv300, xv301)), Just(:(xv400, xv401)), app(ty_[], app(ty_Maybe, eg))) → new_esEs3(xv300, xv400, eg)
new_esEs(@2(xv300, xv301), @2(xv400, xv401), ba, app(ty_Maybe, cb)) → new_esEs3(xv301, xv401, cb)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, he), app(ty_Maybe, bca)), bbb)) → new_esEs3(xv301, xv401, bca)
new_esEs(@2(xv300, xv301), @2(xv400, xv401), ba, app(app(app(ty_@3, bg), bh), ca)) → new_esEs2(xv301, xv401, bg, bh, ca)
new_esEs3(Just(Left(xv300)), Just(Left(xv400)), app(app(ty_Either, app(ty_Maybe, gb)), fb)) → new_esEs3(xv300, xv400, gb)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, ba), app(app(ty_@2, bb), bc))) → new_esEs(xv301, xv401, bb, bc)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, app(app(ty_Either, bbd), bbe), bbb) → new_esEs1(xv301, xv401, bbd, bbe)
new_esEs1(Left(xv300), Left(xv400), app(app(app(ty_@3, fg), fh), ga), fb) → new_esEs2(xv300, xv400, fg, fh, ga)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, he), hf), app(ty_Maybe, bag))) → new_esEs3(xv302, xv402, bag)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, he), app(ty_[], bbc)), bbb)) → new_esEs0(xv301, xv401, bbc)
new_esEs1(Right(xv300), Right(xv400), gc, app(app(app(ty_@3, ha), hb), hc)) → new_esEs2(xv300, xv400, ha, hb, hc)
new_esEs3(Just(Right(xv300)), Just(Right(xv400)), app(app(ty_Either, gc), app(app(app(ty_@3, ha), hb), hc))) → new_esEs2(xv300, xv400, ha, hb, hc)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, app(app(app(ty_@3, bbf), bbg), bbh), bbb) → new_esEs2(xv301, xv401, bbf, bbg, bbh)
new_esEs3(Just(xv30), Just(xv40), app(ty_Maybe, bdc)) → new_esEs3(xv30, xv40, bdc)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_Maybe, bdb), hf, bbb) → new_esEs3(xv300, xv400, bdb)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(app(ty_Either, eb), ec)) → new_esEs1(xv300, xv400, eb, ec)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_Either, bce), bcf), hf, bbb) → new_esEs1(xv300, xv400, bce, bcf)
new_esEs3(Just(Right(xv300)), Just(Right(xv400)), app(app(ty_Either, gc), app(ty_Maybe, hd))) → new_esEs3(xv300, xv400, hd)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(ty_Either, bce), bcf)), hf), bbb)) → new_esEs1(xv300, xv400, bce, bcf)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(app(ty_@2, dg), dh)) → new_esEs(xv300, xv400, dg, dh)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, app(app(ty_@2, bah), bba), bbb) → new_esEs(xv301, xv401, bah, bba)
new_esEs3(Just(Right(xv300)), Just(Right(xv400)), app(app(ty_Either, gc), app(app(ty_@2, gd), ge))) → new_esEs(xv300, xv400, gd, ge)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, he), app(app(app(ty_@3, bbf), bbg), bbh)), bbb)) → new_esEs2(xv301, xv401, bbf, bbg, bbh)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, app(app(ty_@2, cc), cd)), ce)) → new_esEs(xv300, xv400, cc, cd)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(ty_[], ea)) → new_esEs0(xv300, xv400, ea)
new_esEs3(Just(:(xv300, xv301)), Just(:(xv400, xv401)), app(ty_[], df)) → new_esEs0(xv301, xv401, df)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, hf, app(app(ty_@2, hg), hh)) → new_esEs(xv302, xv402, hg, hh)
new_esEs3(Just(:(xv300, xv301)), Just(:(xv400, xv401)), app(ty_[], app(app(app(ty_@3, ed), ee), ef))) → new_esEs2(xv300, xv400, ed, ee, ef)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, app(ty_[], cf)), ce)) → new_esEs0(xv300, xv400, cf)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, ba), app(ty_[], bd))) → new_esEs0(xv301, xv401, bd)
new_esEs3(Just(:(xv300, xv301)), Just(:(xv400, xv401)), app(ty_[], app(app(ty_Either, eb), ec))) → new_esEs1(xv300, xv400, eb, ec)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: